method p2(n: int) returns (x: int, y: int)
requires n > 1
ensures y == n * x + x
{
	assert n > 1; // precondition
	x := 0;
	assert n > 1 && x == 0; // assignment
	y := 0;
	assert n > 1 && x == 0 && y == 0; // assignment
	var i := 0;
	assert n > 1 && x == 0 && y == 0 && i == 0; // assignment
	while i < n
	invariant i <= n
	invariant x == 9 * i
	invariant y == x * i + x
	{
		assert i <= n && x == i * 9 && y == x * i + x; // invariant
		x := x + 9;
		assert i <= n && (x - 9) == i * 9 && y == (x - 9) * i + (x - 9); // assignment
		y := y + 2 * x;
		assert i <= n && (x - 9) == i * 9 && (y - 2 * x) == (x - 9) * i + (x - 9); // assignment
		i := i + 1;
		assert i <= n && x == i * 9 && y == x * i + x; // invariant
	}
	assert i <= n && x == i * 9 && y == x * i + x && i >= n; // invariant and not (guard)
	assert y == n * x + x; // postcondition
	return x, y;
}